p:FinProbSpace, n:, X, Y:RandomVariable(p;n). X  Y   

latex

Definitions	Void, t  T, x:A.B(x), Top, , type List, x:AB(x), x:A. B(x), S  T, P & Q, {x:A| B(x)} , FinProbSpace, Outcome, P  Q, False, A, A  B, i  j < k, , , {i..j}, ||as||, #$n, Type, suptype(S; T), f(a), r  s, , X  Y, RandomVariable(p;n)
Lemmas	qle wf, int seg wf, length wf nat, nat wf, finite-prob-space wf, p-outcome wf, top wf, rationals wf